Nuprl Lemma : list_accum_append
0,22
postcript
pdf
A
,
B
:Top List,
y
,
f
:Top.
list_accum(
x
,
a
.
f
(
x
,
a
);
y
;
A
@
B
) ~ list_accum(
x
,
a
.
f
(
x
,
a
);list_accum(
x
,
a
.
f
(
x
,
a
);
y
;
A
);
B
)
latex
Definitions
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
Top
,
t
T
Lemmas
top
wf
origin
A, B:Top List, y, f:Top.
A, B:Top List, y, f:Top.
x:A. B(x)
x,y. t(x;y)
T